<html>
<head><meta charset="utf-8"><title>Validate atomic fence usages? · general · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/index.html">general</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html">Validate atomic fence usages?</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="164849540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164849540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Charles Lew <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164849540">(May 04 2019 at 04:38)</a>:</h4>
<p>Hi, a friend of mine recently found out in his Rust project that an extremely hard to reoccur deadlock issue is actually caused by incorrect atomic fence usage. I wonder if there're any formal method verification design or tools that can integrate with the language somehow to "reason about" these usages and validate at compile-time that they're correctly used.</p>



<a name="164849555"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164849555" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Charles Lew <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164849555">(May 04 2019 at 04:39)</a>:</h4>
<p><span class="user-mention" data-user-id="120791">@RalfJ</span></p>



<a name="164860351"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164860351" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164860351">(May 04 2019 at 10:06)</a>:</h4>
<p>There is appears to be some research done, mostly around automatic insertion of the memory barriers, but I’m sceptical.</p>



<a name="164860464"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164860464" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164860464">(May 04 2019 at 10:07)</a>:</h4>
<p>See e.g. <a href="http://www.kroening.com/papers/toplas2017-musketeer.pdf" target="_blank" title="http://www.kroening.com/papers/toplas2017-musketeer.pdf">http://www.kroening.com/papers/toplas2017-musketeer.pdf</a></p>



<a name="164860556"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164860556" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nagisa <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164860556">(May 04 2019 at 10:09)</a>:</h4>
<p>I’m not aware of any static analysis tools which would look at your fences and say "hey this one is wrong", but automatic insertion in more general and such an analysis tool could be implemented in terms of such an analysis tool.</p>



<a name="164873437"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164873437" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Charles Lew <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164873437">(May 04 2019 at 15:24)</a>:</h4>
<p><span class="user-mention" data-user-id="123586">@nagisa</span>  thank you!</p>



<a name="164919051"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/122651-general/topic/Validate%20atomic%20fence%20usages%3F/near/164919051" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> RalfJ <a href="https://rust-lang.github.io/zulip_archive/stream/122651-general/topic/Validate.20atomic.20fence.20usages.3F.html#164919051">(May 05 2019 at 13:16)</a>:</h4>
<p>uh... there's probably tools but I dont know much about automated stuff like that, sorry^^</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>